$\forall$${\it da}$:fpf(Knd; $k$.Type). normal{-}da\{i:l\}(${\it da}$) $\in$ prop\{i:l\}